A system and software have recently become more complex and gigantic. As a means for solving the issue, for example, a verification technique by model checking is known. Model checking models a verification target as a state transition system. Then the modeled state transition system is, for example, exhaustively searched. Consequently, for example, whether or not the verification target satisfies a specification is verified. Model checking can be applied from a system design stage. Whether or not the verification target satisfies a specification can also be guaranteed and verified. Accordingly, model checking is attracting attention as a technology for improving reliability of a system and software.
Application of model checking to network verification is also being attempted recently. For example, NPL 1 discloses a system testing, by model checking, a network controlled by OpenFlow. As disclosed in NPL 2 and 3, in OpenFlow, a switch (OpenFlow switch: OFS) performs processing, on the basis of a flow entry set by a controller (OpenFlow controller: OFC). The flow entry specifies, for example, a condition of matching with a predetermined field in a packet header, a rule specifying an operation in the checking, statistical information, and the like. When a flow entry matching with header information in a received packet does not exist with respect to the received packet, the switch, for example, transmits a packet-in message to the controller and requests calculation of a flow. Then, the controller derives a flow, on the basis of a network topology and the like, and sets a flow entry relating to the flow to the switch on the flow.
In NPL 1, when a state search on an OpenFlow network is executed, symbolic execution of an OpenFlow controller program is performed, a set of representative values of packets for executing all code paths is obtained, and a state search is executed by use of the set. An overview of model checking disclosed in NPL 1 will be described in accordance with the description in NPL 1. A system state is assumed to be a combination of component states, and a transition represents a change from one state to another state, such as message transmission. In each state, each component retains a set of feasible transitions. When searching a given state space model, a model checker first initializes a state stack, and subsequently repeats following processing until the state stack becomes empty. The checker selects, from the stack, one state and a transition that is possible in the one state, and tests, for example, a correctness property with respect to a new state newly reached after executing the transition. When the new state does not violate the correctness property, the model checker adds the new state to a searched state set, and schedules execution of all transitions considered feasible in the state. In NPL 1, a program of OpenFlow controller is configured as a set of event handlers, a program state is taken as a value of a global variable, and each event handler is handled as a transition. In order to execute a transition, a corresponding event handler is activated. For example, reception of a packet-in message from the switch enables a packet-in transition, and the model checker executes the transition by activating an event handler corresponding to the transition. Symbolic execution is performed in consideration of an operation of an event handler being data-dependent.
While model checking provides a merit as described above, an amount of memory and time required for calculation increases exponentially with a scale of a verification target. Accordingly, enhanced searching efficiency is essential in model checking aiming at practical verification of a system and software.
For example, NPL 4 discloses dynamic partial order reduction (DPOR) being a technology of pruning a redundant search in view of verification, in model checking with respect to a multi-threaded environment model.
DPOR in a case of searching a state transition system being a model-checking target (such as depth-first-search) is as follows.    (A) Executing an appropriate path first.    (B) Confirming next whether or not there is a pair of transitions, a mutual execution order of which influences an execution result, in a transition sequence of the path. Such a pair of transition is referred to as “transitions in a dependency relation.”    (C) Searching, when the transitions in a dependency relation exist in pairs of transition, for a state immediately before the transition executed earlier of the pair, from the previously executed path, in order to search a path in which an execution order of the transitions in the pair is reversed. Generating next a backtrack point from which a search is started, on the basis of a place where a transition different from the previously executed path (transition different from the transition executed earlier of the pair) is executed from the state (state immediately before the transition executed earlier).    (D) After detecting all transitions in a dependency relation from the previously executed path, resuming the search from the rearmost (at the deepest position) backtrack point on the previously executed path.    (E) Repeating the procedure, (B) to (D) described above, until a backtrack point no longer exists.
Thus, out of all execution patterns of the verification target, only paths having different execution results can be searched. In other words, a search of paths not having a different verification results, that is, redundant paths in view of verification, can be pruned, and enhanced searching efficiency can be provided.
NPL 5 discloses stateful dynamic partial ordering reduction (SDPOR) being a technology improving DPOR. In model checking, in general, when a state searched in the past (searched state) is reached again, a search subsequent to the state is naturally redundant, and therefore the search is discontinued. However, in DPOR, when a search is easily discontinued, analysis of transitions in a dependency relation on an execution path is influenced, and a correct result is not obtained. Accordingly, even when reaching a searched state, DPOR does not discontinue a search and continues the search. SDPOR is improved DPOR, being capable of discontinuing a search when reaching a searched state. SDPOR manages a transition executed in a past search with a graph, and utilizes the graph for analysis of a dependency relation. In the graph, a transition is associated with each node, and each directed edge represents an execution order of transitions executed in a past search.
For example, assuming that a state immediately after a transition t1 executed during the search is s1, when a transition t2 is further executed from s1, a directed edge is drawn in the graph from a node n1 corresponding to the transition t1 to a node n2 corresponding to the transition t2. When reaching a state S2 being searched in the past, SDPOR, in which the nodes n1 and n2 are created when not existent in the graph, checks for a transition executable from the state S2. Additionally, SDPOR searches for a node corresponding to the transition in the graph, and extracts every reachable node by tracing directed edges from the node. A transition corresponding to the previously extracted node represents a transition that may be executed in a state transition after S2. By use of these transitions and a transition on the current execution path, SDPOR analyzes a dependency relation and generates a backtrack point. A merit of SDPOR is, even when a search after a searched state is discontinued, a dependency relation can be correctly analyzed by the procedures, and provides enhanced efficiency can be provided by the discontinuation of the search.
NPL 6 discloses dynamic partial ordering reduction in distributed systems (DPOR-DS) being a technology modifying DPOR, being designed for a multi-threaded system, for model checking of a distributed system. In order to absorb an environmental difference between models being verification targets, DPOR-DS changes a generation method of a backtrack point. With regard to a relation between transitions on an execution path, DPOR-DS defines a happens-before relation in a distributed-environment model aside from a dependency relation, and utilizes the happens-before relation in determination of backtrack point generation. The happens-before relation is an execution-order relation between transitions, always holding on a model. For example, considering transitions transmitting and receiving a packet p, the transition transmitting the packet p always occurs before the transition receiving the packet p. Such an order relation between transitions always holding on the basis of a causal relation on a model is the happens-before relation (refer to NPL 6).
DPOR-DS analyzes existence or nonexistence of a happens-before relation with respect to a transition on an execution path, in addition to a dependency relation. Even in a case that a dependency relation exists between transitions, when a happens-before relation holds, DPOR-DS does not generate a backtrack point. Further, when resuming a search from a backtrack point, out of transitions executed between a pair of two transitions in a dependency relation (denoting the transition executed earlier by t1 and the transition executed later by t2), DPOR-DS successively executes transitions in a happens-before relation with the transition t2, and the transition t2, at the beginning of the resumed search.
With reference to FIG. 1, the above will be described by use of a specific example. It is assumed that transitions ta, tb, tc, and td are executed in this order in a first search. It is further assumed that, as a result of analysis of a dependency relation and a happens-before relation, the following are found:    a dependency relation exists between ta and td, and    a happens-before relation exists between tc and td (tc is always executed before td).
Then, DPOR-DS generates a backtrack point b1 at a state S0 immediately before executing the transition ta.
Then, when resuming the search from the backtrack point b1, DPOR-DS first executes:    tc (the transition in a happens-before relation with the transition [td] executed later of a pair of transitions [ta and td] in a dependency relation, out of the transitions [tb and tc] executed between the pair), and    td (the transition executed later of the pair of transitions in a dependency relation).
Subsequently, there is no specified order of transition, and an appropriate path is executed. Specifically, in the example in FIG. 1, the transitions are executed in an order of, for example, tc, td, ta, and tb from the backtrack point b1. Among the transitions, the first two transitions tc and td constitute a part in which an execution order is specified by a search algorithm of DPOR-DS, as described above. The remaining transitions ta and tb constitute a part in which an execution order is appropriately determined. An order of the pair of transitions in a dependency relation (ta and td) is reversed here. The setting of the order in the first part (tc and td) at the backtrack point is a mechanism aiming at reduction of a redundant search.
With reference to FIG. 2, a situation without the mechanism will be described by use of a specific example. In the example in FIG. 1, in a case that the search is resumed by backtracking, when only one transition (only tc) to be executed first is specified, the transitions may be executed in an order of, for example, tc, ta, tb, and td from the backtrack point b1, as illustrated in FIG. 2.
The backtracking in FIG. 1 aims at execution of a search with a reversed order of ta and td in a dependency relation, while, in the example in FIG. 2, the order of ta and td in a dependency relation is not reversed in the backtracking.
As illustrated in FIG. 2, DPOR-DS analyzes a dependency relation with respect to the path of tc, ta, tb, and td again, and generates a backtrack point b2 at a state s5 immediately before executing the transition ta. Consequently, the transitions are executed in an order of tc, td, ta, and tb in a next search, and a search of a path with transitions generated in a desired order can be provided. However, the second search (search of the path tc, ta, tb, and td) is redundant from the viewpoint of verification and is wasteful from the viewpoint of efficiency. In order to reduce the redundant search, DPOR-DS provides a mechanism of specifying a first transition sequence (the transition sequence tc and td from the backtrack point b1 in the example in FIG. 1) upon resumption of a search by backtracking, to reduce a search of a redundant path (the path tc, ta, tb, and td in the example in FIG. 2). A merit of DPOR-DS is that a search can be pruned in model checking of a distributed-environment model as well, by the procedures.